/-
Copyright (c) 2025 Frédéric Dupuis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Frédéric Dupuis
-/
module

public import Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
public import Mathlib.Algebra.Order.Star.Basic
public import Mathlib.Algebra.Order.Module.Defs
public import Mathlib.Tactic.ContinuousFunctionalCalculus

/-!
# Strictly positive elements of an algebra

This file introduces strictly positive elements of an algebra (also known as positive definite
elements). This is mostly used for C⋆-algebras, but the basic definition makes sense in a more
general context.

## Implementation notes

Note that, while the current definition is adequate in the unital case, it will eventually be
replaced by a definition that makes sense in the non-unital case (an element is strictly
positive if the hereditary C⋆-subalgebra generated by that element is the whole algebra).
Thus, it is best to avoid unfolding the definition and only use the API provided.

## TODO

+ Generalize the definition to non-unital algebras.
-/

@[expose] public section

/-- An element of an ordered algebra is *strictly positive* if it is nonnegative and invertible.

NOTE: This definition will be generalized to the non-unital case in the future; do not unfold
the definition and use the API provided instead to avoid breakage when the refactor happens. -/
def IsStrictlyPositive {A : Type*} [LE A] [Monoid A] [Zero A] (a : A) : Prop :=
  0 ≤ a ∧ IsUnit a

variable {A : Type*}

namespace IsStrictlyPositive

section basic

@[grind =]
lemma iff_of_unital [LE A] [Monoid A] [Zero A] {a : A} :
    IsStrictlyPositive a ↔ 0 ≤ a ∧ IsUnit a := Iff.rfl

@[aesop 20% apply (rule_sets := [CStarAlgebra])]
protected lemma nonneg [LE A] [Monoid A] [Zero A] {a : A} (ha : IsStrictlyPositive a) :
    0 ≤ a := ha.1

@[aesop 20% apply (rule_sets := [CStarAlgebra])]
protected lemma isUnit [LE A] [Monoid A] [Zero A] {a : A} (ha : IsStrictlyPositive a) :
    IsUnit a := ha.2

lemma _root_.IsUnit.isStrictlyPositive [LE A] [Monoid A] [Zero A]
    {a : A} (ha : IsUnit a) (ha₀ : 0 ≤ a) : IsStrictlyPositive a := iff_of_unital.mpr ⟨ha₀, ha⟩

@[grind →]
lemma isSelfAdjoint [Semiring A] [PartialOrder A] [StarRing A] [StarOrderedRing A] {a : A}
    (ha : IsStrictlyPositive a) : IsSelfAdjoint a := ha.nonneg.isSelfAdjoint

@[simp, grind .]
lemma _root_.isStrictlyPositive_one [LE A] [Monoid A] [Zero A] [ZeroLEOneClass A] :
    IsStrictlyPositive (1 : A) := iff_of_unital.mpr ⟨zero_le_one, isUnit_one⟩

end basic

section StarOrderedRing
variable [Semiring A] [StarRing A] [PartialOrder A] [StarOrderedRing A]

lemma _root_.IsUnit.isStrictlyPositive_star_right_conjugate_iff {u a : A} (hu : IsUnit u) :
    IsStrictlyPositive (u * a * star u) ↔ IsStrictlyPositive a := by
  simp_rw [IsStrictlyPositive.iff_of_unital, hu.star_right_conjugate_nonneg_iff]
  lift u to Aˣ using hu
  rw [← Units.coe_star, Units.isUnit_mul_units, Units.isUnit_units_mul]

lemma _root_.IsUnit.isStrictlyPositive_star_left_conjugate_iff {u a : A} (hu : IsUnit u) :
    IsStrictlyPositive (star u * a * u) ↔ IsStrictlyPositive a := by
  simpa using hu.star.isStrictlyPositive_star_right_conjugate_iff

end StarOrderedRing

section Algebra

variable {𝕜 : Type*} [Ring A] [PartialOrder A]

@[grind ←, aesop safe apply]
protected lemma smul [Semifield 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜}
    (hc : 0 < c) {a : A} (ha : IsStrictlyPositive a) :
    IsStrictlyPositive (c • a) := by
  have hunit : IsUnit (c • a) :=
    isUnit_iff_exists.mpr ⟨c⁻¹ • ha.isUnit.unit⁻¹, by simp [(ne_of_lt hc).symm]⟩
  exact hunit.isStrictlyPositive (smul_nonneg hc.le ha.nonneg)

@[grind ←, aesop safe apply]
lemma _root_.isStrictlyPositive_algebraMap [ZeroLEOneClass A] [Semifield 𝕜] [PartialOrder 𝕜]
    [Algebra 𝕜 A] [PosSMulMono 𝕜 A] {c : 𝕜} (hc : 0 < c) :
    IsStrictlyPositive (algebraMap 𝕜 A c) := by
  rw [Algebra.algebraMap_eq_smul_one]
  exact IsStrictlyPositive.smul hc isStrictlyPositive_one

lemma spectrum_pos [CommSemiring 𝕜] [PartialOrder 𝕜] [Algebra 𝕜 A]
    [NonnegSpectrumClass 𝕜 A] {a : A} (ha : IsStrictlyPositive a) {x : 𝕜}
    (hx : x ∈ spectrum 𝕜 a) : 0 < x := by
  have h₁ : 0 ≤ x := by grind
  have h₂ : x ≠ 0 := by grind [= spectrum.zero_notMem_iff]
  exact lt_of_le_of_ne h₁ h₂.symm

grind_pattern IsStrictlyPositive.spectrum_pos => x ∈ spectrum 𝕜 a, IsStrictlyPositive a

end Algebra

end IsStrictlyPositive
